es:ES, P:(E).
(e:E. Dec(P(e)))
 (X:AbsInterface(E)
 ((e:E.
 ((((e  X))  (a:E. (es-p-le-pred(es;P)(e,a))))
 (& (((e  X))  (es-p-le-pred(es;P)(e,X(e)))))) 

latex

Definitions	t  T, Dec(P), x:AB(x), Type, , x:A. B(x), P  Q, x:A  B(x), x:A. B(x), ES, s = t, x.A(x), strong-subtype(A;B), AbsInterface(A), b, P  Q, P & Q, es-p-le-pred(es;P), f(a), x,y. t(x;y), E
Lemmas	assert wf, iff wf, es-interface wf, event system wf, es-interface-from-decidable, es-p-le-pred wf, decidable wf, decidable exists-es-p-le-pred, es-E wf